 /**
 * 
 */
package extensionTools.smvCreator;

import java.util.ArrayList;
import java.util.HashSet;

import extensionTools.smvCreator.Exceptions.RulesUtilsException;
import extensionTools.smvCreator.Exceptions.SmvDBException;
import extensionTools.smvCreator.Link.LinkType;
import extensionTools.smvCreator.Link.SmvType;

/**
 * @author Oshrit & Lital & Luba
 *
 */
public class EvProcess extends Rule {
	
	public HashSet<String> evInvokeVariables = new HashSet<String>();
	
	class ObjectCond
	{
		String name, value;
		LinkType type;
		ObjectCond(String name, String value, LinkType type)
		{
			this.name = name;
			this.value = value;		
			this.type = type;
		}
		
	}
	
	class Var
	{
		Var()
		{
			this.part = new ArrayList<EvProcess.ObjectCond>();
		}
		String variable;
		ArrayList<ObjectCond> part;
	}
	//This is the return string - here all the function could use it.
	String rules;
        public EvProcess(DiagramDatabase db) {
                super(db);
        }
        

        /* (non-Javadoc)
         * @see extensionTools.smvCreator.Rule#createRule()
         */
        @Override
        public String createRule() throws RulesUtilsException, SmvDBException 
        {
            rules = "";
            String waitForState ="";
            //String waitForProc = "";
			HashSet<String> waitForProcs = new HashSet<String>();
            for (SmvProcess currProc : db.getSmvProcessList()) 
        	{

                String procName = currProc.getName();
                
                //Create the rule only for process who have father processes
                if (currProc.getFatherId() == -1)
                {
                        waitForState = "notActive";
                        waitForProcs.add(procName);
                }
                else 
                {
                        SmvProcess prevProc = RulesUtils.getPrevProcessId(currProc, db);

                        //If the previous process is above the currProc in the timeline,
                        //(the two processes have the same fatherId), the waiting event occurs when
                        //the above process is in notActive state
                        if (prevProc != null) 
                        {
    
                        	//String prevProcName = prevProc.getName();
                        		//If the previous process is above the current process in the timeline
                                if (prevProc.getFatherId() == currProc.getFatherId())
                                {
                                        //ArrayList<String> prevProcList = RulesUtils.getProcsInSameTimeline(prevProc, db);	
									    waitForProcs = RulesUtils.getProcsInSameTimeline(prevProc, db);
										waitForState = "notActive";
                                }
                                //Otherwise, the previous process is the father process,
                                //and the waiting event occurs when the father becomes active
                                else 
                                {
                                	waitForState = "active";
                                    waitForProcs.add(prevProc.getName());
                                }
                        }
                }

                ArrayList<ObjectCond> activateCondition = new ArrayList<ObjectCond>();
                for(Link link : currProc.getLinkList())
            	{
                	State srcState;
                	SmvObject srcObject;
                	switch (link.getLinkType()){
                	case CONDITION:
                		srcState = db.getSmvStateList().get((db.findStateById(link.getSrcId())));
                		srcObject = db.getSmvObjectList().get((db.findObjectById(srcState.getObjectId())));
            			activateCondition.add(new ObjectCond(srcObject.getName(), srcState.getName(), LinkType.CONDITION));
                	break;
                	case INSTRUMENT:
                		if(link.getSrcType() == SmvType.STATE)
                		{
	                		srcState = db.getSmvStateList().get((db.findStateById(link.getSrcId())));
	                		srcObject = db.getSmvObjectList().get((db.findObjectById(srcState.getObjectId())));
                			activateCondition.add(new ObjectCond(srcObject.getName(), srcState.getName(), link.getLinkType()));	
                		}
                		else //srcType is an object
                		{
                			srcObject = db.getSmvObjectList().get((db.findObjectById(link.getSrcId())));
                			activateCondition.add(new ObjectCond(srcObject.getName(), "notExist", link.getLinkType()));		                			
                		}
            		break;
                	case CONSUMPTION:
                		//only if there is no label on the link!!!
                		if(link.getLabel() == "")
                		{
                    		if(link.getSrcType() == SmvType.STATE)
                    		{
    	                		srcState = db.getSmvStateList().get((db.findStateById(link.getSrcId())));
    	                		srcObject = db.getSmvObjectList().get((db.findObjectById(srcState.getObjectId())));
                    			activateCondition.add(new ObjectCond(srcObject.getName(), srcState.getName(), link.getLinkType()));	
                    		}
                    		else //srcType is an object
                    		{
                    			srcObject = db.getSmvObjectList().get((db.findObjectById(link.getSrcId())));
                    			activateCondition.add(new ObjectCond(srcObject.getName(), "notExist", link.getLinkType()));		                			
                    		}
                		}               		
                	break;
                	//creating invocation next rule
                	case INVOCATION:
                		SmvProcess srcProc = RulesUtils.getProccessbyId(link.getSrcId(), db);
                		SmvProcess dstProc = RulesUtils.getProccessbyId(link.getDstId(), db);
                		if(srcProc == null || dstProc == null) throw new SmvDBException("EvProcess: Invocation link didn't find the link edges");
                		if(srcProc == currProc)
                				createInvokeRule(dstProc,currProc);
                	break;
                	}
                	
            	}
               
	          ArrayList<Var> objectCond = new ArrayList<Var>();
             
              
        	  if (activateCondition.size() > 0)
        	  {
	              ArrayList<String> binaryNumbers = new ArrayList<String>(); 
	              for(int i=0; i< Math.pow(2,activateCondition.size()); i++)
	              {
	            	  String str = Integer.toBinaryString(i);
	            	  while(str.length() < activateCondition.size())
	            	  {
	            		  str = "0".concat(str);
	            	  }
	            	  binaryNumbers.add(str);
	              }
	              
	              for (String str : binaryNumbers)
	              {
	            	  Var cond = new Var();
	                  cond.variable = "";
	            	  for(int i=0; i<str.length(); i++)
	            	  {
	            		  if(cond.variable == "") cond.variable = "!("+ activateCondition.get(i).name + "_" + str.substring(i, i+1) + " = " + activateCondition.get(i).value + ")";
	            		 // else cond.variable = SmvOp.and("!("+ cond.variable, activateCondition.get(i).name + "_" + str.substring(i, i+1) + " = " + activateCondition.get(i).value+")");
	            		  else cond.variable =  cond.variable + " & " +  "!("  + activateCondition.get(i).name + "_" + str.substring(i, i+1) + " = " + activateCondition.get(i).value + ")";
	            		  
	            		  cond.part.add(new ObjectCond(activateCondition.get(i).name + "_" + str.substring(i, i+1), activateCondition.get(i).value, activateCondition.get(i).type));
	            	  }	      
	            	  objectCond.add(cond);	            	  
	              }
        	  }
            
        	//*** EV_ACTIVATE ***//
        	for (int i=0; i<SMVCreator.K; i++)
            {
        		rules += "\n" + createActivationCase(currProc, objectCond , i);
        	}
    
        	//*** EV_TERMINATE ***//

    		ArrayList<ObjectCond> isCond = new ArrayList<ObjectCond>(); 
    		for(int index=0; index<objectCond.size();index++)
    		{	    			                 
                  //condition link not happen - > notActive
 	              isCond = isCondition(objectCond.get(index).part, isCond);
    		}
    		  
        	for (int i=0; i<SMVCreator.K; i++)
            {
        		  rules += "\n" + createTerminationCase(currProc, isCond , i);  
	     	}
              
        	//*** EV_WAITING ***//
            for (int i=0; i<SMVCreator.K; i++)
            {
            	rules += "\n" + createWaitCase(currProc, waitForProcs, waitForState, i);       
            }
            waitForProcs.removeAll(waitForProcs);
            
        	//*** EV_HALT ***//
            for (int i=0; i<SMVCreator.K; i++)
            {
            	rules += "\n" + createHaltCase(currProc, i);       	
            }
        }
        return rules;
    }
    
     /**
      *    
      * @param currProc the current smv process. Checks if objects with instrument link are exist - if not wait for the next loop,
      *  Check that all conditions are true - if not the process terminate (seee createTermintionCase).
      * @param objectCond
      * @param i the current instance
      * @return an ev_activate rule
      * @throws RulesUtilsException
      */
     private String createActivationCase(SmvProcess currProc, ArrayList<Var> objectCond, int i) throws RulesUtilsException{
     	 
    	 String procName = currProc.getName();
    	 ArrayList<String> ruleForEv = new ArrayList<String>();
		 String procNameIns = procName + "_" + i; 
		 String evName = "ev_activate_" + procNameIns;
		 for(int index=0; index<objectCond.size();index++)
		 {
			 String father = db.getProcessNameById(currProc.getFatherId());
		  
			 String assoc = "";
			 for(ObjectCond c : objectCond.get(index).part)
			 {
				 String assocType = "";
				 if (c.type == LinkType.INSTRUMENT)
				 {
					 assocType = "assocInstrument_";
				 }
				 else if(c.type == LinkType.CONDITION)
				 {
					 assocType = "assocCondition_";
				 }
				 else
				 {
					 assocType = "assoc_";
				 }
				 if (assoc == "") assoc = assocType + c.name + "_" + father + "_"+ i + "=" + "TRUE";
				 else assoc = SmvOp.and(assoc, assocType + c.name + "_" + father + "_"+ i + "=" + "TRUE");
         	 }
			  
			 
       	  	 //ev_active: all links happen -> active
             ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event1", procNameIns + " = waiting", 
            		 objectCond.get(index).variable, assoc), "TRUE"));
         }
		 if(objectCond.size() == 0)
		 {
			 ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event1", procNameIns + " = waiting"), "TRUE"));			  
         }
         ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event2", procNameIns + " = active"), "FALSE"));
		 ruleForEv.add(SmvOp.createCaseLine("TRUE", evName));
		 return SmvOp.next(evName, SmvOp.createCase(RulesUtils.arrayListToArray(ruleForEv)));
     }
    
     /**
      * This method created the case for the termination event. First add all conditions related to the
      * activation of the process and if one of them are not true the process get terminate- all the condition are condition link in the diagram and are been saved 
      * in  isCond Array in createRule function. Then add all rules related to termination of process
      * (children that are not active and etc).
      * @param currProc the current smv process
      * @param isCond
      * @param i the current instance
      * @return an ev_terminate case
      * @throws RulesUtilsException
      */
     private String createTerminationCase(SmvProcess currProc, ArrayList<ObjectCond> isCond, int i) throws RulesUtilsException {
    	  
     	 String procName = currProc.getName();
    	 ArrayList<String> ruleForEv = new ArrayList<String>();
		 String procNameIns = procName + "_" + i; 
		 String evName = "ev_terminate_" + procNameIns; 
		 String father = db.getProcessNameById(currProc.getFatherId());
         for(ObjectCond c : isCond)
         {
        	 
        	 ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event1", procNameIns + " = waiting",
        			  "!(" + c.name + "=" + c.value + ")", "assocCondition_" + c.name + "_" + father + "_" + i + "=" + "TRUE"), "0"));
         }

 		 //Doing the event rule for termination
         String rule = SmvOp.and(procNameIns + " = active ", "sysState = event1");
         String childRestrict = createChildRestrictions(db.getChildrenList(currProc), i);
         if (childRestrict != null) 
         {
             rule = SmvOp.and(rule, childRestrict);
         }
     
         String res = SmvOp.prepareTerminationRes(db.getEvTerm());

         //Doing the process rule for termination
         ruleForEv.add(SmvOp.createCaseLine(rule, res));
         //this one is for the case where we de-activated process at the last period
         ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event2",procNameIns + " = notActive"),"1"));
         ruleForEv.add(SmvOp.createCaseLine(evName + " = 0", "0")); 
         ruleForEv.add(SmvOp.createCaseLine("TRUE", "1"));
         return SmvOp.next(evName, SmvOp.createCase(RulesUtils.arrayListToArray(ruleForEv))); 
     }
        
        
     /**
     * This method created the case for the waiting event
     * @param currProc the current smv process
     * @param waitForProcs a set of processes the current process need to wait for them to
     * become notActive (if they are above it in the timeline) , or to become active (if the current
     * process is first in its timeline and is waiting for its father process
     * @param waitForState
     * @param i the current instance
     * @return an ev_wait case
     * @throws RulesUtilsException
     */
    private String createWaitCase(SmvProcess currProc, HashSet<String> waitForProcs,
    		String waitForState, int i ) throws RulesUtilsException 
    {
    	
    	String procName = currProc.getName();
    	String procFullName = procName + "_" +i;
        ArrayList<String> ruleForEv = new ArrayList<String>();
        
        String evName = "ev_wait_" + procFullName;
		ArrayList<String> waitingRules = RulesUtils.createWaitProcessCondition(waitForProcs, i, waitForState, db);
		for (String rule : waitingRules) {
        	ruleForEv.add(rule);
        }
		//ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event1", condition), "TRUE"));
		ArrayList<String> evInvokeRelevantVariables = new ArrayList<String>();

		//Check all ev_invoke variable in the system and find the relevant ones for
		//the current process
		HashSet<String> InvokeVariable = SystemInit.getInvokeVariables();
		if (InvokeVariable != null) {
			for (String currInvoke : InvokeVariable) {
				if (currInvoke.endsWith(procFullName)) {
					evInvokeRelevantVariables.add(currInvoke);
				}
			}
		}
		if (evInvokeRelevantVariables != null) {
			for (String currInvoke : evInvokeRelevantVariables){
				ruleForEv.add(SmvOp.createCaseLine(SmvOp.and(SmvOp.and("sysState = event1", currInvoke + " = TRUE"), 
						procFullName + " = notActive"),	"FALSE")  );
			}
		}
        ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event2", procFullName + " = waiting"), "FALSE"));
        ruleForEv.add(SmvOp.createCaseLine("TRUE", "FALSE"));
        return SmvOp.next(evName, SmvOp.createCase(RulesUtils.arrayListToArray(ruleForEv)));
    }
    
    /**
     * This method implements the Halt event - when a process' brother (a different process
     * in the same timeline) has an ev_invoke event, the process halts    
     * @param currProc the current smv process
     * @param i the current instance
     * @return an ev_halt case
     * @throws RulesUtilsException
     */
    private String createHaltCase(SmvProcess currProc, int i ) throws RulesUtilsException
    {
    	String procName = currProc.getName();
    	String procFullName = procName + "_" +i;
		String eventName = "ev_halt_" + procFullName;
		ArrayList<String> ruleForEv = new ArrayList<String>();
	    //Find all the processes in the same timeline as the current process
		//and check if they have evInvoke variable that are on
		HashSet<String> brotherProcs = RulesUtils.getProcsInSameTimeline(currProc, db);
	    if (brotherProcs != null) {
	    	for (String brother : brotherProcs) {
	    		if (brother != currProc.getName()) {
	    			ArrayList<String> evInvokes = getEvInvokeVarsByPrefix("ev_invoke_" + brother + "_"+ i);
	    			if (evInvokes != null) {
	        			for (String evInvoke : evInvokes) {
	        				ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event1", 
	     					       evInvoke + " = TRUE"), "TRUE"));
	        			}
	    			}
	    		}
	    	}
	    }
	    //Check if an ancestor of the process got ev_invoke
	    ArrayList<String> ancestors = RulesUtils.getAllAncestorProcs(currProc, db);
	    if (ancestors != null) {
		    for (String ancestor : ancestors) {
	        	ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event2", 
	        				"ev_halt_" + ancestor + "_" + i + " = TRUE"), "TRUE"));
	        }
	    }
	    if (ruleForEv.size() > 0) {
	    	ruleForEv.add(SmvOp.createCaseLine(SmvOp.and("sysState = event2", 
				       eventName + " = TRUE"), "FALSE"));
	    	ruleForEv.add(SmvOp.createCaseLine("TRUE", eventName));
	    	return SmvOp.next(eventName, SmvOp.createCase(RulesUtils.arrayListToArray(ruleForEv)));
	    }
	    return "";
    }
        
    /**
     *     
     * @param prefix a prefix string
     * @return all evInvoke variables which names' begin with prefix
     */
    private ArrayList<String> getEvInvokeVarsByPrefix(String prefix) {
    	ArrayList<String> result = new ArrayList<String>();
    	
    	for (String evInvoke : SystemInit.getInvokeVariables()) {
			if (evInvoke.startsWith(prefix)) {
				result.add(evInvoke);
			}
		}
    	return result;
    }
     
    /**
     * This function builds the "next" case for the invocation rule
     * @param event
     * @param currProc
     * @throws RulesUtilsException - when null parameters were sent to SmvOp
     */
    private void createInvokeRule(SmvProcess dstProc, SmvProcess currProc) throws RulesUtilsException {
			String invokeRule = "";
			for (int i=0; i<SMVCreator.K; i++){
    			for(int j=0; j<SMVCreator.K;j++){
    				String event = "ev_invoke_"+currProc.getName()+"_"+i+"_"+dstProc.getName()+"_"+j;
    				evInvokeVariables.add(event);
    				String currRule = SmvOp.and("sysState = event2","ev_terminate_"+currProc.getName()+"_"+i + " = 0");
    				String dieRule = SmvOp.and("sysState = event2",SmvOp.not("ev_terminate_"+currProc.getName()+"_"+i + " = 0"));
        			currRule = SmvOp.createCaseS(SmvOp.createCaseLine(currRule,"TRUE"),SmvOp.createCaseLine(dieRule,"FALSE"),SmvOp.createCaseLine("TRUE",event));
    				invokeRule+=SmvOp.next(event, currRule);
    			}
    		}			
			rules+=invokeRule;
		}


	private ArrayList<ObjectCond> isCondition(ArrayList<ObjectCond> part, ArrayList<ObjectCond> isCond) 
    {
    	boolean flag = true;
    	for (int i =0; i<part.size(); i++)
    	{
    		flag = true;
    		if(part.get(i).type == LinkType.CONDITION)
    		{
    			for(ObjectCond c : isCond)
    			{
    				if(c.name.equals(part.get(i).name))
    				{
    					flag = false;
    					break;
    				}
    			}
    			if(flag) isCond.add(part.get(i));
    		}
    	}
			
		return isCond;
	}
	/**
     * This function create the condition on children
     * the terminate rule for process is valid if all the 
     * children of the process is not active. 
     * @param children
     * @param i
     * @return the rules that the children make
     */
    private String createChildRestrictions(ArrayList<SmvProcess> children, int i)
    {
            String childLines = null;
            for (SmvProcess child : children) 
            {
                String childName = child.getName();
                //In case it's the first child
                if (childLines == null)
                    {
                            childLines = childName + "_" + i+" = notActive";
                    }
                childLines = SmvOp.and(childLines, childName + "_" + i+" = notActive");
            }
            return childLines;
    }
    
    
}


